RAZONAMIENTO AUTOMÁTICO

“La causalidad no opera hacia atrás” (Gregory Bateson)

“La lógica nació como un intento de mecanizar los procesos intelectivos del razonamiento (D. Hofstadter)

“La matemática pronto será hecha solo por ordenadores” (Boris Shaliach)

“La lógica es combinar lo conocido para alcanzar lo desconocido” (George Edward Moore)

---

Tipos de Razonamiento
Razonamiento como modo de conciencia analítica

Como sabemos, hay dos modos de conciencia:

• Descendente (top-down), deductiva, analítica o sintáctica. Va de lo general a lo particular, de lo profundo a lo superficial. Corresponde al modo del hemisferio izquierdo (HI) del cerebro.
  
  
• Ascendente (bottom-up), inductiva, sintética o semántica. Va desde los hechos particulares a los generales (o de los generales a más generales o universales), de lo superficial a lo profundo. La mente humana, en su aspecto sintético, conceptualiza, buscando siempre las categorías más generales a los hechos particulares para que la realidad sea inteligible. Si no las encuentra, busca un patrón secundario que relacione las categorías. La inducción puede ser completa (cuando se examinan todos los casos) o incompleta (cuando no se examinan todos). Corresponde al modo del hemisferio derecho (HD) del cerebro.

Razonar es utilizar el modo HI, ir de lo general a lo particular, la capacidad de realizar inferencias o deducciones. Para ello, todo debe ser expresado en un lenguaje formal. El razonamiento hace explícito un conocimiento que ya está implícito en las premisas o en la base de conocimientos.


La automatización del razonamiento

La conciencia inductiva incompleta en principio no se puede automatizar porque lo intuitivo no se puede formalizar; solo se pueden formalizar sus manifestaciones. La conciencia sintética es objeto de estudio de la psicología cognitiva, siendo hoy día uno de los principales desafíos de la inteligencia artificial.

En cambio, la conciencia analítica puede ser automatizada, pues es puramente formal. El razonamiento automático es una rama de la ciencia de la computación que estudia las capacidades de razonamiento de los sistemas computacionales.


El concepto de inferencia

La inferencia es el proceso de derivar conclusiones a partir de un conjunto de premisas (o derivar teoremas a partir de axiomas). Las premisas, las conclusiones y el propio proceso de inferencia deben expresarse en un lenguaje formal, que puede ser natural o artificial. Las premisas o axiomas pueden ser de tipo general o específico, así como las conclusiones.

Suponiendo que el proceso de inferencia sea correcto, las inferencias pueden ser válidas, aunque las premisas sean falsas. Pero de la verdad de las premisas siempre se producen inferencias verdaderas.

Una inferencia es monótona si no varía al añadir nuevas premisas. En caso contrario, es no-monótona.


Tipos de razonamiento con reglas

Una base de conocimientos está formada por:

1. Un conjunto de premisas o axiomas de una teoría, expresados en un lenguaje formal. Si estas premisas se expresan mediante reglas del tipo “condición → acción” o “antecedente → consecuente”, tenemos una base de reglas, que representan el conocimiento genérico.
   
   
2. Un conjunto de hechos, que forman una base de hechos. Representan el conocimiento específico.

En esta base de conocimientos hay dos tipos de razonamiento:

1. Directo (o hacia adelante).
   Se van examinando los antecedentes de las reglas, y cuando se cumplen, se obtienen inferencias, que son los consecuentes. Las reglas se vuelven a aplicar a las inferencias obtenidas para obtener nuevas inferencias. Y así sucesivamente hasta que las reglas no produzcan nuevas inferencias.
   
   
2. Inverso (o hacia atrás).
   Se parte del objetivo (una sentencia o expresión) y se examinan las reglas que contienen ese objetivo en los consecuentes de las reglas. Si no se encuentra ninguna regla, es imposible alcanzar el objetivo. Si se encuentran, se elige una de ellas y el antecedente de esa regla se convierte en el nuevo objetivo. Y así sucesivamente en un proceso recursivo. Cuando una regla no conduce al objetivo, se elige otra regla alternativa (si existe). Este tipo de razonamiento es el que se utiliza en la programación lógica.

Estos dos tipos de razonamiento son análogos a los utilizados en el cálculo aritmético. Por ejemplo: 1) Directo: 3² = 9 (se realiza la operación de elevar 3 al cuadrado); 2) Inverso: √9 = 3 (se busca un número tal que su cuadrado sea 9),

El razonamiento directo es más fácil de automatizar que el inverso, de la misma manera que es más fácil realizar operaciones directas que las inversas.

La ventaja del razonamiento directo es que todas las expresiones que se van infiriendo se van incorporando a la base de conocimientos. La desventaja es que las expresiones inferidas son la base para obtener más inferencias, un proceso que tiende a crecer exponencialmente.

La ventaja del razonamiento inverso es que conocemos el objetivo, la expresión a demostrar, y evitamos explorar reglas innecesarias. La desventaja es que los pasos que vamos dando no están garantizados, teniendo que retroceder a menudo para encontrar el camino correcto que nos conducirá al objetivo. Cuando es aplicable, el razonamiento inverso es más eficiente que el razonamiento directo porque no se tienen que hacer múltiples pasadas por el conjunto de las reglas.

Lo ideal es utilizar ambos métodos de manera controlada, según el tema o problema que se trate.


La gestión del razonamiento automático

La gestión del razonamiento, tanto directo como inverso, se realiza con un programa o “motor” de razonamiento. Este motor puede ser específico para cada sistema particular o bien ser genérico (o universal), válido para todo sistema. Lo ideal es que se pueda desarrollar un motor universal, es decir, independientemente del contenido de las reglas.

El razonamiento automático es independiente del dispositivo mecánico con el que se implementa. Computar es una actividad que puede ser humana o mecánica, pero conceptualmente es la misma cosa. La informática o la ciencia de la computación no se reduce a la tecnología de los ordenadores, de la misma manera que las astronomía no se reduce a la tecnología de los telescopios. Ordenadores y telescopios son solo instrumentos de sus respectivas ciencias.

El motor de razonamiento realiza dos funciones:

1. El examen de cada regla para ver si es aplicable. Si el motor es de razonamiento directo, examina el antecedente. Si el motor es razonamiento inverso, examina el consecuente. El motor de inferencia para el razonamiento hacia adelante explora las reglas en amplitud, es decir, se consideran todas las reglas, independientes entre sí. Para el razonamiento hacia atrás, las reglas se examinan en profundidad, es decir, se parte de una regla y se busca una regla dependiente de ella.
   
   
2. El control, que gestiona el orden en que se examinan las reglas.

Demostración automática de teoremas

Las demostraciones automáticas de teoremas (DAT) −en inglés, Automated Theorem Proving, ATP− es un tipo de razonamiento inverso. Se fundamentan en la lógica formal. Actualmente es el campo más desarrollado del razonamiento automatizado.

El procedimiento consiste en 3 pasos: 1) el usuario expresa una conjetura mediante un expresión del lenguaje formal; 2) esta expresión se la pasa al sistema computacional como entrada; 3) el sistema intenta resolverlo; 4) si se resuelve, la respuesta puede ser positiva o negativa (la conjetura es o no es un teorema).

Un demostrador de teoremas parte del teorema a demostrar y el demostrador descubre (o infiere) los pasos a realizar para llegar desde los axiomas al teorema.

Una demostración puede servir para demostrar que algo es verdadero o para demostrar que algo es falso. Refutar es demostrar una negación.

Mediante la automatización de la demostración de teoremas se han encontrado nuevos teoremas no conocidos previamente. También se han descubierto algunas demostraciones más cortas y elegantes que las humanas.


Campos de aplicación

Los campos de aplicación del razonamiento automático son numerosos, siendo los más importantes:

• Matemática. Demostración de teoremas matemáticos en álgebra booleana, teoría de grupos, teoría de redes, geometría algebraica, lógica combinatoria, etc.
  
  
• Informática. Diseño y gestión de bases de datos, generación y verificación de programas, programación lógica.
  
  
• Inteligencia artificial. Sistemas expertos, ingeniería del conocimiento, robótica, agentes inteligentes.
  
  
• Internet. Web semántica.
  
  
• Circuitos eléctricos. Diseño y verificación de circuitos integrados (por ejemplo, para verificar que las operaciones matemáticas se han diseñado correctamente, especialmente las operaciones más complejas, como las de punto flotante.
  
  
• Lingüística. Proceso del lenguaje natural.

Una breve historia del razonamiento automático

• La teoría de la deducción formal nació con la lógica silogística aristotélica, realizada en lenguaje natural.
  
  
• Hacia finales del siglo XVII, Leibniz postula la necesidad de un lenguaje formal universal (Lingua Characteristica Universalis) para poder expresar cualquier idea. Este lenguaje debería servir también para mecanizar cualquier tipo de razonamiento (Calculus Ratiocinator). Leibniz afirmaba que el razonamiento es como el cálculo, y que en lugar de largas discusiones, sería mejor sentarse a calcular para determinar quien tenía razón en cada caso.
  
  Leibniz creía que se podía formalizar un sistema coherente de lógica y matemática mediante un lenguaje constituido por un alfabeto de símbolos manipulados por reglas mecánicas. Anticipándose a lo que hoy denominamos “software”, afirmaba que la lógica y la matemática se podían mecanizar. Con su Calculus Ratiocinator, Leibniz creía que todas las verdades de la razón se podían descubrir de forma mecánica.
  
  Según Leibniz, nuestro universo habría sido creado mediante un mínimo número de leyes que condujeron a una máxima diversidad. Que la aritmética binaria encarnaba ese principio: solo dos signos bastan para escribir todos los números; lo finito engendra por combinatoria lo infinito. Que la codificación binaria era la clave del lenguaje universal, pues no solo permitía representar los números sino también la lógica de las dicotomías. Que mediante la computación digital la humanidad tendría un poderoso instrumento para aumentar el poder de la mente.
  
  
• En 1847, George Boole inventa el álgebra de la lógica (reduciendo la lógica al álgebra), un primer paso para la mecanización de los procesos de pensamiento lógico.
  
  
• En 1879, Frege publica su Begriffsschrift (Conceptografía), naciendo la lógica formal, la lógica matemática moderna con el cálculo de predicados. Su obra “Fundamentos de Aritmética” (publicada en 1884) la expresó mediante la lógica formal, inaugurando la corriente logicista de la matemática (la lógica como fundamento de la matemática).
  
  
• En 1889, Peano publica Arithmetices Principia, en el que utiliza una notación simbólica para formalizar la aritmética, una teoría de primer orden que recoge las propiedades de los números naturales.
  
  
• A comienzos del siglo XX, Cantor inventa la teoría de conjuntos. El lenguaje matemático queda reducido y fundamentado en la lógica de predicados y la teoría de conjuntos.
  
  
• También a principios del siglo XX, Hilbert propone fundamentar la matemática mediante un sistema metamatemático, un sistema axiomático universal, del cual se derivaría toda la matemática. Según Hilbert, toda la matemática se puede deducir de un sistema axiomático universal formado por unos pocos axiomas y unas pocas reglas de inferencia. Hilbert había inventado un sistema axiomático formal para la lógica proposicional basado en 3 axiomas y una regla de inferencia (ver Adenda).
  
  
• En los años 1910-1913, Russell y Whitehead, siguiendo la línea logicista inaugurada por Frege, publicaron Principia Mathematica, obra que fue revisada (en una segunda edición) en 1927. Estos autores creían que podían derivar toda la matemática a partir de solo 4 axiomas lógicos, 3 axiomas de la teoría de conjuntos y 2 reglas de transformación.
  
  
• En 1929, Gödel demuestra que la lógica de predicados de primer orden es completa, es decir, que toda fórmula válida es demostrable. Las fórmulas válidas son recursivamente numerables.
  
  
• En 1929, Mojzesz Presburger demuestra que la teoría de los números naturales con adición e igualdad es decidible, y dio un algoritmo para determinar si una sentencia dada del lenguaje era verdadera o falsa.
  
  
• En 1930, Jacques Herbrand publica el artículo “Investigation in proof theory” [Herbrand, 1930]. En él propone un método automático para demostrar teoremas de la lógica de predicados de primer orden. Este método producía un crecimiento exponencial de inferencias (los denominados “universos Herbrand”).
  
  
• En 1931, Gödel publica su teorema de incompletud, en el que demuestra que un sistema axiomático formal que incluya a los números naturales es incompleto: hay sentencias indecidibles (no es posible demostrar su verdad o falsedad). Gödel utilizó para demostrarlo una expresión autorreferente, una expresión imposible de alcanzar a través de los axiomas, por muy numerosos que estos sean. Con el teorema de Gódel se invalida el logicismo en general y los proyectos de Hilbert y de Principia Mathematica en particular.
  
  
• En 1934, Gerhard Gentzen inventa la Deducción Natural y el Cálculo de Secuentes, una teoría y una práctica orientada a emular el razonamiento humano de las demostraciones matemáticas. El nivel semántico es superior al álgebra de Boole, pero las demostraciones son más complejas. Gentzen rompió la formalización axiomática tradicional de Frege, Hilbert y Russell.
  
  
• Tras la segunda Guerra Mundial, aparecen los ordenadores electrónicos, y con los avances en lógica matemática, se retoma con fuerza el tema del razonamiento automático, convirtiéndose en uno de los principales temas de la inteligencia artificial.
  
  
• En 1957, Allen Newell, Herbert Simon y Clifford Shaw presentan su Logic Theorist Machine, un programa de ordenador que fue capaz de demostrar 38 de los 52 teoremas de la lógica proposicional de Principia Mathematica de Russell y Whitehead. Este programa fue el primer programa de inteligencia artificial y utilizaba un pequeño número de axiomas y reglas de inferencia heurísticas.
  
  
• En 1959, P.C. Gilmore, utilizando formas normales disyuntivas (disyunción de conjunciones), logró muchas demostraciones automáticas de fórmulas de la lógica de primer orden (sin igualdad) mediante el método de reducir una fórmula de primer orden a otra fórmula proposicional asociada a ella [Gilmore, 1959].
  
  
• En 1960, Martin Davis y Hillary Putnam publican “A computing procedure for quantification theory”, en el que proponen un algoritmo o procedimiento de inferencia completo para fórmulas expresadas en forma normal conjuntiva (conjunción de disyunciones) [Davis & Putnam, 1960]. Introdujeron el concepto de “cláusula” (una disyunción de fórmulas con predicados, afirmativos o negativos, cuantificados universalmente) y redujeron las demostraciones de primer orden al estudio de la consistencia de conjuntos finitos de cláusulas proposicionales, mediante reglas simplificadoras. Sin embargo, el algoritmo generaba un espacio de búsqueda demasiado grande.
  
  
• En 1960, Hao Wang desarrolló un programa de ordenador con el que consiguió demostrar 220 teoremas de Principia Mathematica, incluyendo teoremas de la lógica de predicados de primer orden, usando el sistema de deducción natural de Gerhard Gentzen (cálculo de secuentes sin reglas de corte). Su método era más refinado que el de Davis y Putnam, y su programa era más eficiente que del la máquina de lógica teórica porque utilizaba heurísticas [Wang, 1960, 1970].
  
  
• En 1965, John Alan Robinson publica “A machine-oriented logic based on the Resolution Principle” [Robinson, 1965], en donde introduce el Principio de Resolución, un método que reduce significativamente el proceso de razonamiento de manera eficiente. Los axiomas se expresan en forma disyuntiva. Utiliza el método refutativo (reducción al absurdo): se parte de la negación de lo que se quiere demostrar, y si se llega a una contradicción, es que el teorema es verdadero.
  
  El método de Robinson es consistente y completo. “Completo” quiere decir que si tenemos un conjunto de sentencias e insatisfacible (falso), el método de resolución deriva la cláusula vacía, indicando que existe una contradicción.
  
  El principio de resolución es muy simple, pues se basa en una sola regla, en el que dos cláusulas padres se sustituyen por una cláusula resolvente:
  
  
  Premisas: A∨B y ¬A. Conclusión: B.
  
  Esta regla se generaliza en el principio de resolución binaria:
  
  
  Premisas: A∨B y ¬A∨C. Conclusión: B∨C.
  
  Y su forma más general es:
  
  
  Premisas: A∨B₁∨…∨B_n y ¬A∨C₁∨…∨C_m. Conclusión: B₁∨…∨B_n∨C₁∨…∨C_m.
  
  Junto al método de resolución, Robinson presentó un algoritmo de unificación, que maximizaba la generalidad de las inferencias. El algoritmo de unificación identifica pares de términos complementarios (una constante y una variable) y realiza una sustitución (de la variable por la constante) para eliminar las diferencias. Es un algoritmo recursivo: genera resolventes, resolventes de resolventes, etc., hasta llegar a la cláusula vacía.
  
  El método de Robinson supuso un hito y dio un gran impulso al tema de la demostración automática de teoremas. Sin embargo, el método de Robinson presenta varias limitaciones:
  
  
  1. Puede funcionar en la lógica de predicados de primer orden, pero siempre que se utilicen variables libres (las que pueden tener cualquier valor), que implícitamente están cuantificadas universalmente.
     
     
  2. No funciona con la lógica de orden superior.
     
     
  3. En la práctica, se produce una “explosión demográfica” de cláusulas,incluyendo cláusulas irrelevantes o redundantes, por lo que el espacio de búsqueda para encontrar una solución es muy grande (incluso para demostrar teoremas simples), por lo que a veces no se llega a una solución en tiempo razonable.
  
  El método de resolución de Robinson ha sido mejorado (refinado) a lo largo de los años y ha conducido a una gran variedad de heurísticas (también denominadas “estrategias”) para reducir el espacio de búsqueda. Una forma de reducir el espacio de búsqueda es restringir la regla de inferencia para que se generen menos inferencias, pero manteniendo la completud del procedimiento.
  
  
• En 1970 se demuestra el teorema de los 4 colores (4 colores son suficientes para colorear un mapa) mediante un programa de ordenador que examinó exhaustivamente todos los tipos de combinaciones posibles. Fue motivo de gran controversia, ya que fue la primera demostración automática que fue imposible de comprobar a nivel humano debido al enorme tamaño de los cálculos realizados por el programa.
  
  
• A principios de los 1970s, inspirado por el método de resolución de Robinson, Robert Kowalski introduce la programación lógica, abriendo el camino al lenguaje Prolog [Kowalski, 1979].

Está en marcha una iniciativa europea de investigación en el campo de la demostración de teoremas de manera eficiente y precisa. El proyecto se denomina TPTP (Thousands of Problems for Problem Solvers, http://www.tptp.org). Se ha creado un nuevo lenguaje también denominado TPTP en el que expresar problemas y soluciones mediante la lógica de orden superior. Y también un formato denominado THF (Typed Higher-order Form).

Hoy día, se puede considerar que el ideal de Leibniz se ha logrado en gran medida. No obstante, aún queda todavía mucho por hacer: investigar nuevas heurísticas, nuevos algoritmos más eficientes, nuevas reglas (o meta-reglas), etc.

Hoy día no hay discusiones sobre aritmética cuando se utiliza una calculadora. Pero la calculadora, aunque dé la respuesta correcta, no la demuestra, es decir, no muestra todos los pasos que da para llegar a un resultado. Lo ideal es que con el razonamiento se logre el mismo resultado.


MENTAL y el Razonamiento Automático
Los sistemas tradicionales de razonamiento automático se basan:

• En la lógica proposicional o en la lógica de predicados de primer orden.
  
  
• La base de conocimientos genéricos está limitada a reglas.
  
  
• Se necesita un motor de inferencias para gestionar la base de conocimientos genéricos a partir de la base de conocimientos específicos y producir las inferencias.

En cambio, en MENTAL:

• Las expresiones pueden ser de cualquier tipo, no solo lógicas. Además, las expresiones lógicas pueden tener predicados de cualquier orden.
  
  
• La base de conocimientos genéricos se basa en expresiones genéricas.
  
  
• No se necesita ningún motor de inferencias porque las inferencias son automáticas por la propia semántica de las expresiones genéricas.

En realidad, el problema de las inferencias se puede plantear de manera general. Un proceso de inferencia es un proceso de evaluación normal de una expresión que produce una modificación del espacio abstracto. Si la expresión original no cambia, todas las nuevas expresiones generadas son las inferencias producidas.


Lenguaje universal

El problema del razonamiento automático es que no es posible abordarlo de manera coherente sin un lenguaje formal estándar y universal, donde el lenguaje matemático-lógico sea igual al de los ordenadores. Con MENTAL como lenguaje universal, este problema desaparece y se está en condiciones idóneas para abordar el tema del razonamiento automático.

Taradicionalmente, en el razonamiento automático se ha considerado un lenguaje formal basado en la lógica de predicados de primer orden con igualdad, un lenguaje con el que se podía formalizar muchas áreas de la matemática. Pero este lenguaje dista mucho de ser universal y no es el lenguaje de los ordenadores.

Características de MENTAL como lenguaje universal para el razonamiento automático son:

• Utiliza expresiones genéricas, que tienen un enorme poder integrador y unificador. Las expresiones genéricas (parametrizadas o no) permiten realizar razonamientos automáticos (directos e inversos) porque realizan el examen y el control de las reglas desde un nivel superior. No se necesita ningún “motor de razonamiento” hacia adelante ni hacia atrás porque el motor está implícito en el lenguaje. También permite expresar heurísticas.
  
  
• La lógica está basada en la primitiva “Condición”. Negación, conjunción y disyunción son operaciones derivadas. También se puede utilizar la lógica de orden superior.
  
  
• Los predicados son atributos o calificadores externos que pueden aplicarse a cualquier expresión. Por ejemplo, “Sócrates/mortal”. Las propiedades son cualidades internas (por ejemplo, la propiedad de que un nombre empiece por “A”, la propiedad de que un nombre tenga longitud 4, o la propiedad de un número de ser mayor que 3), etc.
  
  
• No hay cuantificadores lógicos. El papel del cuantificador universal lo desempeña un parámetro de una expresión genérica. El cuantificador existencial es una propiedad (la cardinalidad) de un conjunto o secuencia.
  
  
• No hay expresiones condicionales específicas. Antecedente y consecuente de una condición pueden ser expresiones cualesquiera.
  
  
• No contempla los valores lógicos tradicionales (verdadero y falso). En su lugar contempla valores existenciales (existencia y no existencia). No se considera el tema de la verdad sino solo el tema de la existencia o no existencia de una expresión.
  
  
• Se distingue claramente entre expresiones particulares y generales.
  
  
• Se utiliza la equivalencia y la sustitución junto con el resto de las primitivas semánticas.
  
  
• La deducción pueden ser dinámicas, en el sentido de que las inferencias varían cuando cambian las expresiones.

La formalización de una demostración

Tradicionalmente, las premisas y la conclusión se representan de forma vertical:

A₁
,,,
A_n
---------
C

Por ejemplo, la regla de resolución binaria de Robinson se expresa así:

A∨B
¬A∨C
---------
B∨C

El problema de esta representación es que no se utiliza un lenguaje formal que relacione las premisas y la conclusión.

En MENTAL, este problema se resuelve fácilmente gracias a la semántica de la operación “Condición”. Por ejemplo, la regla de Robinson anterior se puede expresar como una expresión genérica:

⟨( A∨B → ¬A∨C → B∨C)⟩

Esta expresión es equivalente a
⟨( (A∨B ∧ ¬A∨C) → B∨C)⟩
En donde ⟨( ¬A = (A?)' )⟩


La codificación de las reglas

Con el objeto de que el proceso sea lo más eficiente posible y exista correspondencia con el tipo de razonamiento a realizar, las reglas se especifican mediante expresiones genéricas de la forma siguiente:

• Razonamiento hacia adelante:
  ⟨( A1 → ... → An → C )⟩
  
  
• Razonamiento hacia atrás:
  ⟨( C ← A1 ← ... ← An )⟩

siendo las Ai los antecedentes y C el consecuente. Estas expresiones tienen la ventaja de que cuando no se cumple un antecedente, se termina el proceso de análisis de esa regla. Es lo que se denomina “corte”.

En el razonamiento hacia adelante va desde el antecedentes hacia los consecuentes. El razonamiento hacia atrás va desde el consecuente hacia los antecedentes.

Como la evaluación es de izquierda a derecha, en el razonamiento inverso se pone en primer lugar lo que se quiere demostrar.

Puede haber varias expresiones con el mismo C, es decir, que existan alternativas: a la conclusión se puede llegar por varios caminos posibles. Y lo mismo le ocurre con los antecedentes.

Esta estructura de reglas es equivalente a las cláusulas de Horn, la que se utiliza en programación lógica, que tienen la forma

c ← a₁, a₂, ... , a_n o bien, a₁, a₂, ... , a_n → c

en donde las comas suponen conexiones lógicas “y” (and).

Las reglas pueden interactuar entre sí como activarse o desactivarse, limitarse con condiciones adicionales, etc.


Tipos de inferencias

Las inferencias se realizan mediante los operadores de condición (→, ← y ↔), los operadores de sustitución (=, =: y :=) y el operador de equivalencia (≡).

Las inferencias van de lo general a lo particular y pueden ser de dos tipos:

1. Horizontales. Se realizan a través de los operadores simétricos (↔ y ≡).
   
   
2. Verticales descendentes. Se realizan a través de las operaciones de condición y de sustitución.

Tipos de expresiones

En MENTAL podemos clasificar las expresiones en 3 tipos:

1. Expresiones tipo A. Son las expresiones genéricas (parametrizadas o no), que son los motores de las inferencias.
   
   
2. Expresiones tipo B. Son expresiones genéricas (parametrizadas o no) o no genéricas que son las expresiones iniciales a partir de las cuales se realizan las inferencias.
   
   
3. Expresiones tipo C. Son las inferencias realizadas mediante las expresiones de los dos tipos anteriores.

Las expresiones tipo B se especifican detrás de las de tipo A para que se evalúen de forma inmediata y que producen las expresiones de tipo C.


Características de las inferencias

• Puede no haber expresiones de tipo B, es decir, las expresiones de tipo A son suficientes para realizar inferencias.
  
  
• Toda expresión de MENTAL se evalúa y puede o no generar inferencias. Las inferencias (C) pueden ser expresiones generales o particulares, dependiendo de las expresiones genéricas A y B. Una expresión puede dar lugar a varias expresiones inferidas.
  
  
• Puede no haber expresiones de tipo C (inferencias nulas), es decir, no hay nuevas expresiones.
  
  
• En MENTAL no se utiliza solo la lógica, sino toda expresión genérica que involucre a los operadores mencionados. La inferencia está implícita en la semántica de las expresiones genéricas.
  
  
• En MENTAL, las inferencias pueden ser monótonas o no monótonas, dependiendo de las expresiones utilizadas. No-monónicidad quiere decir que las inferencias pueden variar a medida que se modifican las expresiones A o las expresiones B.
  
  En general, las inferencias son dinámicas, en el sentido de que una expresión X puede inferir otra expresión Y, y posteriormente la misma expresión X inferir otra expresión diferente Z o no inferir nada.
  
  
• En la inferencia se puede producir un crecimiento exponencial de las expresiones en el espacio abstracto, pero hoy día este problema no es demasiado importante por el abaratamiento de la memoria y el crecimiento de la capacidad de proceso de los ordenadores. Además, se pueden imponer restricciones para limitar las inferencias automáticas, incluyendo heurísticas o condiciones adicionales a las expresiones genéricas.
  
  
• No hay proceso de búsqueda. Se trata solo de saber si una expresión existe o no en el espacio abstracto. La búsqueda es un tema implementador. A nivel conceptual, las expresiones genéricas son suficientes.

Ejemplos

1. Expresiones tipo A.
   ⟨( x/hombre → x/mortal )⟩ // modus ponens
   
   Expresiones tipo B.
   Sócrates/hombre
   
   Expresiones tipo C (inferencias).
   Sócrates/mortal
   
   
2. Expresiones tipo A.
   ⟨( a = b )⟩ // sustitución
⟨( b = c )⟩ // sustitución
   
   Expresiones tipo B.
   Ninguna.
   
   Expresiones tipo C (inferencias).
   ⟨( a = c )⟩ // ley transitiva de la sustitución
   
   
3. Expresiones tipo A.
   ⟨( x+y ≡ y+x )⟩ // ley conmutativa de la suma
   
   Expresiones tipo B.
   a+b
⟨a+x⟩
   
   Expresiones tipo C (inferencias).
   (a+b ≡ b+a)
(⟨a+x⟩ ≡ ⟨x+a⟩)
   
   
4. Expresiones tipo A.
   ⟨( x → x∨y )⟩ // ley de la lógica
   
   Expresiones tipo B.
   a
   
   Expresiones tipo C (inferencias).
   ⟨( a → a∨y )⟩
   
   
5. Expresiones tipo A.
   ⟨( x*y ≡ y*x )⟩ // ley conmutativa del producto

⟨( (x+y)*z ≡ (x*z + y*z) )⟩ // ley distributiva
   
   Expresiones tipo B.
   Ninguna.
   
   Expresiones tipo C (inferencias).
   ⟨( (x+y)*z ≡ (z*x + z*y) )⟩
⟨( (x+y)*z ≡ (x*z + z*y) )⟩
⟨( (x+y)*z ≡ (z*x + y*z) )⟩
⟨( (x+y)*z ≡ (x*z + y*z) )⟩

⟨( z*(x+y) ≡ (x*z + y*z) )⟩
⟨( z*(x+y) ≡ (z*x + z*y) )⟩
⟨( z*(x+y) ≡ (x*z + z*y) )⟩
⟨( z*(x+y) ≡ (z*x + y*z) )⟩
   
   Este es un ejemplo de inferencias que producen expresiones genéricas.
   
   
6. Expresiones tipo A.
   ⟨( (x+y)*z ≡ (x*z + y*z) )⟩ // ley distributiva

⟨( x^2 =: x*x )⟩
   
   Expresiones tipo B.
   (a+b)^2
   
   Expresiones tipo C (inferencias).
   ( (a+b)^2 =: (a^2 + 2*a*b + b^2) )
   
   
7. Expresiones tipo A.
   ⟨( x∧y → x )⟩ // ley de la lógica

⟨( x∧y ↔ y∧x )⟩ // ley conmutativa de la conjunción lógica
   
   Expresiones tipo B.
   a∧b
   
   Expresiones tipo C (inferencias).
   b∧a
a
b
   
   
8. Expresiones tipo A.
   ⟨( x∈(C∩D) ↔ (x∈C ∧ x∈D) )⟩
   
   Expresiones tipo B.
   a∈(A∩B)
   
   Expresiones tipo C (inferencias).
   a∈A
a∈B
   
   
9. Expresiones tipo A.
   ⟨( (x ∨ y) ≡ (x' ∧ y')' )⟩ // primera ley de De Morgan

⟨( (x ≡ y') ↔ (x' ≡ y) )⟩
   
   Expresiones tipo C (inferencias).
   ⟨( (x ∨ y)' ≡ (x' ∧ y') )⟩

⟨( (x' ∨ y')' ≡ (x ∧ y) )⟩ // segunda ley de De Morgan

Gestión de las expresiones genéricas

• Activación/desactivación de una expresión genérica.
  Se pueden controlar las inferencias de las expresiones genéricas utilizando un variable que indique la activación o no de dichas expresiones genéricas. Por ejemplo:
  
  ⟨( k=1 → ⟨( f(x) = (2^x + 1) )⟩ )⟩
  k=1 // activar expresión genérica ⟨( f(x) = (2^x + 1) )⟩ )⟩

f(3) // ev. 7

k=0 // desactivar expresión genérica

f(3) // se autoevalúa
  
  
• Sustitución de una expresión genérica G1 por otra G2:
  
  
  ( p = G1 )
⟨p⟩
( p = G2⟩ )
  
  
• Eliminación de una expresión genérica G.
  
  
  ( p = G )
⟨p⟩
( p = θ⟩ )

Ejemplo de razonamiento directo e inverso

Se parte de una expresión (bien formada) G, genérica (parametrizada o no) o específica, de la que se quiere saber si es válida o no.

El proceso es automático, pues las expresiones genéricas se evalúan en todo momento. Por lo tanto, si G aparece como consecuente en algún axioma, automáticamente se autoevaluará si se cumple la condición asociada. Si esa condición depende a su vez de otra condición, se aplica el mismo proceso, y así sucesivamente. Las condiciones que no se cumplen se evaluarán como  (la expresión nula). Ejemplo:

Se define (P(x) = y) como “el padre de x es y”.

Se define (H(x) = y) como “el hijo de x es y”.

Se define (A(x) = y) como “el abuelo de x es y”.

Base de conocimientos para el razonamiento directo:

Hechos:
(P(a) = b) (P(b) = c)

Reglas:
⟨( (P(x) = y) ↔ (H(y) = x) )⟩
⟨( (P(x) = y) → (P(y) = z) → (A(x) = z))⟩

Consulta de la base de conocimientos:

(A(a) = c)? // ev. α
(A(a) = b)? // ev. θ

Base de conocimientos para el razonamiento inverso:

(P(a) = b) (P(b) = c)
⟨( (A(x) = y) ← {⟨( z ← (P(x) = z) → (P(z) = y) )⟩}# > 0) )⟩

Consulta de la base de conocimientos:

(A(a) = c)? // ev. α
(A(a) = b)? // ev. θ

Conclusiones

La idea de Leibniz de crear un lenguaje universal se puede decir que se ha cumplido con MENTAL, al fundamentarse en un número mínimo de conceptos que producen potencialmente infinitas expresiones. Pero no se fundamenta en el cálculo binario, sino en arquetipos primarios duales. La dualidad es universal. Los números binarios son solo la manifestación más simple de esa dualidad.

Y también se ha realizado con MENTAL la idea de Leibniz de que ese lenguaje universal fuera capaz de realizar cálculos. Esos cálculos se especifican mediante expresiones genéricas, que son autosuficientes como motores para el razonamiento automático.

---

Adenda
El sistema deductivo de Hilbert

El sistema deductivo de Hilbert para la lógica proposicional tiene las características siguientes:

• Consta de solo 3 axiomas (tautologías) en los que solo se consideran las conectivas lógicas “¬” y “→”:
  
  
  1. p→(q→p)
  2. (p→(q→r))→((p→q)→(p→r)) (distribución)
  3. (¬p→¬q)→((¬p→q)→p)
  
  
• Tiene una sola regla de inferencia: el Modus Ponens: p, p→q ⇒ q.
  
  
• Una deducción formal es una secuencia finita de fórmulas de la lógica proposicional en donde cada fórmula es una instancia de un axioma o la aplicacion de la regla de inferencia a dos fórmulas anteriores.

Por ejemplo, queremos demostrar: p→p:

1. Instanciación del axioma 1 con p=p y q=(p→p): p→((p→p)→p)
   
   
2. Instanciación del axioma 2 con p=p, q=(p→p) y r=p: p→((p→p)→p))→
   ((p→(p→p))→(p→p))
   
   
3. Aplicando el Modus Ponens entre 1 y 2: (p→(p→p))→(p→p)
   
   
4. Instanciado el axioma 1 con p=p y q=p: p→(p→p)
   
   
5. Aplicando el Modus Ponens entre 3 y 4: (p→p)

Bibliografía

• Bibel, W. Automated Theorem Proving. Vieweg Verlag, 1987.
  
  
• Bledsoe, W.W. Non-resolution theorem proving. Artificial Intelligence 9(1), 1977.
  
  
• Boyer, R.S.; Moore, J.S. A Computational Logic Handbook. Academic Press, 1988.
  
  
• Buss, Samuel R. An introduction to proof theory. En Buss, Samuel R. (ed.), Handbook of proof theory, pp. 1-78, Elsevier 1998.
  
  
• Chang, C.L., Lee, R.C.-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1997.
  
  
• Cuena Bartolomé, José. Lógica Informática. Alianza Editorial, 1985.
  
  
• Gardner, Martin. Máquinas y diagramas lógicos. Alianza Editorial, 1985.
  
  
• Gilmore, P.C. A procedure for the production from axioms, of proofs for theories derivable within the first order predicate calculus. Proc. IFIP Congr. 1959, pp. 265-273, 1959.
  
  
• Hogger, C.J. Introduction to Logic Programming. Academic Press, 1984.
  
  
• Kowalski, Robert. Logic for Problem Solving. Elsevier, 1979.
  
  
• Kowalski, Robert. Lógica, Programación e Inteligencia Artificial. Diaz de Santos, 1986.
  
  
• Kowalski, Robert. The case for using equality axioms in automatic demostration. Lecture Notes in Maths, 125: 112-127, 1970.
  
  
• Lassez, Jean Louis; Plotkin, Gordon (eds.). Computational Logic. Essays in Honor of Alan Robinson. The MIT Press, 1991.
  
  
• Loveland, D.W. Automated Theorem Proving. A Logical Basis. North Holland, 1978.
  
  
• Nilsson, N.J. Problem Solving Methods in Artificial Intelligence. McGraw Hill, 1971.
  
  
• Portoraro, Frederic, Automated Reasoning. En Edward N. Zalta, Stanford Encyclopedia of Philosophy.
  
  
• Robinson, John Alan. A machine-oriented logic based on the resolution principle. J. ACM 12 (1): 23-41, 1965.
  
  
• Robinson, John Alan. Automated Deduction with Hyperresolution. International Journal of Com. Mach, 1: 227-234, 1965.
  
  
• Robinson, John Alan; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. The MIT Press, 2001.
  
  
• Robinson, John Alan. Computational Logic: The Unification Computation. Internet, 1971.
  
  
• Slagle, J.R. Automatic Theorem Proving with Renamable and Semantic Resolution. JACM 14: 687-697, 1967.
  
  
• Tarski, Alfred. Introduction to Logic and the Methodology of Deductive Sciences. Dover, 1995.
  
  
• Veroff, Robert (ed.). Automated Reasoning and Its Applications. Essays in Honor of Larry Wos. The MIT Press, 1997.
  
  
• Wang, Hao. Proving Theorems by Pattern Recognition I. Communications of the ACM, 3: 220-234, 1960. Disponible online.
  
  
• Wos, Larry. Automated Reasoning: Introduction and Applications. McGraw-Hill, 1992.
  
  
• Wos, Larry. J.A. Robinson, a review of Automatic Theorem-Proving. Journal of Symbolic Logic 39 (1): 190, 1974.
  
  
• Wang, Hao. Logic, Computers, and Sets. Chelsea Pub. Co., 1970.